home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / scheme / schmrprt / r4rs.lha / sem.tex (.txt) < prev    next >
Encoding:
LaTeX Document  |  1991-11-08  |  23.7 KB  |  576 lines
  1. %\vfill\eject
  2. \section{Formal semantics}
  3. \label{formalsemanticssection}
  4. \bgroup
  5. \newcommand{\sembrack}[1]{[\![#1]\!]}
  6. \newcommand{\fun}[1]{\hbox{\it #1}}
  7. \newenvironment{semfun}{\begin{tabbing}$}{$\end{tabbing}}
  8. \newcommand\LOC{{\tt{}L}}
  9. \newcommand\NAT{{\tt{}N}}
  10. \newcommand\TRU{{\tt{}T}}
  11. \newcommand\SYM{{\tt{}Q}}
  12. \newcommand\CHR{{\tt{}H}}
  13. \newcommand\NUM{{\tt{}R}}
  14. \newcommand\FUN{{\tt{}F}}
  15. \newcommand\EXP{{\tt{}E}}
  16. \newcommand\STV{{\tt{}E}}
  17. \newcommand\STO{{\tt{}S}}
  18. \newcommand\ENV{{\tt{}U}}
  19. \newcommand\ANS{{\tt{}A}}
  20. \newcommand\ERR{{\tt{}X}}
  21. \newcommand\EC{{\tt{}K}}
  22. \newcommand\CC{{\tt{}C}}
  23. \newcommand\MSC{{\tt{}M}}
  24. \newcommand\PAI{\hbox{\EXP$_{\rm p}$}}
  25. \newcommand\VEC{\hbox{\EXP$_{\rm v}$}}
  26. \newcommand\STR{\hbox{\EXP$_{\rm s}$}}
  27. \newcommand\elt{\downarrow}
  28. \newcommand\drop{\dagger}
  29. %\newcommand\injekt{\hbox{ \rm in }}
  30. %\newcommand\projekt{\,\vert\,}
  31. This section provides a formal denotational semantics for the primitive
  32. expressions of Scheme and selected built-in procedures.  The concepts
  33. and notation used here are described in~\cite{Stoy77}; the notation is
  34. summarized below:
  35. \begin{tabular}{ll}
  36. $\langle\,\ldots\,\rangle$ & sequence formation \\
  37. $s \elt k$               & $k$th member of the sequence $s$ (1-based) \\
  38. $\#s$               & length of sequence $s$ \\
  39. $s \:\S\: t$               & concatenation of sequences $s$ and $t$ \\
  40. $s \drop k$                & drop the first $k$ members of sequence $s$ \\
  41. $t \rightarrow a, b$       & McCarthy conditional ``if $t$ then $a$ else $b$'' \\
  42. $\rho[x/i]$               & substitution ``$\rho$ with $x$ for $i$'' \\
  43. $x\hbox{ \rm in }{\tt{}D}$         & injection of $x$ into domain ${\tt{}D}$ \\
  44. $x\,\vert\,{\tt{}D}$       & projection of $x$ to domain ${\tt{}D}$
  45. \end{tabular}
  46. The reason that expression continuations take sequences of values instead
  47. of single values is to simplify the formal treatment of procedure calls
  48. and to make it easy to add multiple return values.
  49. The boolean flag associated with pairs, vectors, and strings will be true
  50. for mutable objects and false for immutable objects.
  51. The order of evaluation within a call is unspecified.  We mimic that
  52. here by applying arbitrary permutations {\it permute} and {\it
  53. unpermute}, which must be inverses, to the arguments in a call before
  54. and after they are evaluated.  This is not quite right since it suggests,
  55. incorrectly, that the order of evaluation is constant throughout a program (for
  56. any given number of arguments), but it is a closer approximation to the intended
  57. semantics than a left-to-right evaluation would be.
  58. The storage allocator {\it new} is implementation-dependent, but it must
  59. obey the following axiom:  if \hbox{$\fun{new}\:\sigma\:\elem\:\LOC$}, then
  60. $\sigma\:(\fun{new}\:\sigma\:\vert\:\LOC)\elt 2 = {\it false}$.
  61. \def\P{\hbox{\rm P}}
  62. \def\I{\hbox{\rm I}}
  63. \def\Ksem{\hbox{$\cal K$}}
  64. \def\Esem{\hbox{$\cal E$}}
  65. The definition of $\Ksem$ is omitted because an accurate definition of
  66. $\Ksem$ would complicate the semantics without being very interesting.
  67. If \P{} is a program in which all variables are defined before being
  68. referenced or assigned, then the meaning of \P{} is
  69. $$\Esem\sembrack{\hbox{\tt((\ide{lambda} (\arbno{\I}) \P')
  70. \hyper{undefined} \dotsfoo)}}$$
  71. where \arbno{\I} is the sequence of variables defined in \P, $\P'$
  72. is the sequence of expressions obtained by replacing every definition
  73. in \P{} by an assignment, \hyper{undefined} is an expression that evaluates
  74. to \fun{undefined}, and
  75. $\Esem$ is the semantic function that assigns meaning to expressions.
  76. %The semantics in this section was translated by machine from an
  77. %executable version of the semantics written in Scheme itself.
  78. %[This was once true, but then I modified the semantics without
  79. %going back to the executable version.  -- Will]
  80. \subsection{Abstract syntax}
  81. \def\K{\hbox{\rm K}}
  82. \def\I{\hbox{\rm I}}
  83. \def\E{\hbox{\rm E}}
  84. \def\C{\hbox{$\Gamma$}}
  85. \def\Con{\hbox{\rm Con}}
  86. \def\Ide{\hbox{\rm Ide}}
  87. \def\Exp{\hbox{\rm Exp}}
  88. \def\Com{\hbox{\rm Com}}
  89. \def\|{$\vert$}
  90. \begin{tabular}{r@{ }c@{ }l@{\qquad}l}
  91. \K & \elem & \Con & constants, including quotations \\
  92. \I & \elem & \Ide & identifiers (variables) \\
  93. \E & \elem & \Exp & expressions\\
  94. \C & \elem & \Com{} $=$ \Exp & commands
  95. \end{tabular}
  96. \setbox0=\hbox{\tt\Exp{} \goesto{}}  %\tt for spacing
  97. \setbox1=\hbox to 1\wd0{\hfil \|}
  98. \begin{grammar}
  99. \Exp{} \goesto{} \K{} \| \I{} \| (\E$_0$ \arbno{\E})
  100.  \copy1{} (lambda (\arbno{\I}) \arbno{\C} \E$_0$)
  101.  \copy1{} (lambda (\arbno{\I} {\bf.}\ \I) \arbno{\C} \E$_0$)
  102.  \copy1{} (lambda \I{} \arbno{\C} \E$_0$)
  103.  \copy1{} (if \E$_0$ \E$_1$ \E$_2$) \| (if \E$_0$ \E$_1$)
  104.  \copy1{} (set! \I{} \E)
  105. \end{grammar}
  106. \subsection{Domain equations}
  107. \begin{tabular}{@{}r@{ }c@{ }l@{ }l@{ }ll}
  108. $\alpha$   & \elem & \LOC & &          & locations \\
  109. $\nu$      & \elem & \NAT & &          & natural numbers \\
  110.            &       & \TRU &=& $\{$\it false, true$\}$ & booleans \\
  111.            &       & \SYM & &          & symbols \\
  112.            &       & \CHR & &          & characters \\
  113.            &       & \NUM & &          & numbers \\
  114.            &       & \PAI &=& $\LOC \times \LOC \times \TRU$  & pairs \\
  115.            &       & \VEC &=& $\arbno{\LOC} \times \TRU$ & vectors \\
  116.            &       & \STR &=& $\arbno{\LOC} \times \TRU$ & strings \\
  117.        &       & \MSC &=& \makebox[0pt][l]{$\{$\it false, true, 
  118.                                 null, undefined, unspecified$\}$} \\
  119.        &       &      & &          & miscellaneous \\
  120. $\phi$     & \elem & \FUN &=& $\LOC\times(\arbno{\EXP} \to \EC \to \CC)$
  121.                                        & procedure values \\
  122. $\epsilon$ & \elem & \EXP &=& \makebox[0pt][l]{$\SYM+\CHR+\NUM+\PAI+\VEC+\STR+\MSC+\FUN$}\\
  123.        &       &      & &          & expressed values \\
  124. %          &       & \STV &=& \EXP     & stored values \\
  125. $\sigma$   & \elem & \STO &=& $\LOC\to(\STV\times\TRU)$ & stores \\
  126. $\rho$       & \elem & \ENV &=& $\Ide\to\LOC$  & environments \\
  127. $\theta$   & \elem & \CC  &=& $\STO\to\ANS$  & command continuations \\
  128. $\kappa$   & \elem & \EC  &=& $\arbno{\EXP}\to\CC$ & expression continuations \\
  129.        &       & \ANS & &             & answers \\
  130.        &       & \ERR & &             & errors
  131. \end{tabular}
  132. \subsection{Semantic functions}
  133. \def\Ksem{\hbox{$\cal K$}}
  134. \def\Esem{\hbox{$\cal E$}}
  135. \def\Csem{\hbox{$\cal C$}}
  136. \begin{tabular}{@{}r@{ }l}
  137.   $\Ksem:$ & $\Con\to\EXP$  \\
  138.   $\Esem:$ & $\Exp\to\ENV\to\EC\to\CC$ \\
  139. $\arbno{\Esem}:$ & $\arbno{\Exp}\to\ENV\to\EC\to\CC$ \\
  140.   $\Csem:$ & $\arbno{\Com}\to\ENV\to\CC\to\CC$
  141. \end{tabular}
  142. % thin \,  medium \> [or \:]   thick \;
  143. \renewcommand{\:}{\mskip\medmuskip}
  144. \newcommand{\wrong}[1]{\fun{wrong }\hbox{\rm``#1''}}
  145. \newcommand{\go}[1]{\hbox{\hspace*{#1em}}}
  146. \bgroup\small
  147. \vspace{1ex}
  148. Definition of \Ksem{} deliberately omitted.
  149. \begin{semfun}
  150. \Esem\sembrack{\K} =
  151.   \lambda\rho\kappa\:.\:\fun{send}\,(\Ksem\sembrack{\K})\,\kappa
  152. \end{semfun}
  153. \begin{semfun}
  154. \Esem\sembrack{\I} = 
  155.   \lambda\rho\kappa\:.\:\fun{hold}\:
  156.     $\=$(\fun{lookup}\:\rho\:\I)$\\
  157.      \>$(\fun{single}(\lambda\epsilon\:.\:
  158.         $\=$\epsilon = \fun{undefined}\rightarrow$\\
  159.      \>  \> \go{2}$\wrong{undefined variable},$\\
  160.      \>  \>\go{1}$\fun{send}\:\epsilon\:\kappa))
  161. \end{semfun}
  162. \begin{semfun}
  163. \Esem\sembrack{\hbox{\tt($\E_0$ \arbno{\E})}} =$\\
  164.  \go{1}$\lambda\rho\kappa\:.\:\arbno{\Esem}
  165.     $\=$(\fun{permute}(\langle\E_0\rangle\:\S\:\arbno{\E}))$\\
  166.      \>$\rho\:$\\
  167.      \>$(\lambda\arbno{\epsilon}\:.\:
  168.         ($\=$(\lambda\arbno{\epsilon}\:.\:
  169.                  \fun{applicate}\:(\arbno{\epsilon}\elt 1)
  170.                  \:(\arbno{\epsilon}\drop 1)
  171.                 \:\kappa)$\\
  172.      \>   \>$(\fun{unpermute}\:\arbno{\epsilon})))
  173. \end{semfun}
  174. \begin{semfun}
  175. \Esem\sembrack{\hbox{\tt(\ide{lambda} (\arbno{\I}) \arbno{\C} $\E_0$)}} =$\\
  176.  \go{1}$\lambda\rho\kappa\:.\:\lambda\sigma\:.\:$\\
  177.   \go{2}$\fun{new}\:\sigma\:\elem\:\LOC\rightarrow$\\
  178.    \go{3}$\fun{send}\:
  179.      $\=$(\langle
  180.          $\=$\fun{new}\:\sigma\,\vert\,\LOC,$\\
  181.       \>  \>$\lambda\arbno{\epsilon}\kappa^\prime\:.\:
  182.            $\=$\#\arbno{\epsilon} = \#{\arbno{\I}}\rightarrow$\\
  183.       \>  \>    \>$\go{1}\fun{tievals}
  184.            $\=$(\lambda\arbno{\alpha}\:.\:
  185.              $\=$(\lambda\rho^\prime\:.\:\Csem\sembrack{\arbno{\C}}\rho^\prime
  186.                   (\Esem\sembrack{\E_0}\rho^\prime\kappa^\prime))$\\
  187.       \>  \>    \>  \>    \>$(\fun{extends}\:\rho\:{\arbno{\I}}\:\arbno{\alpha}))$\\
  188.       \>  \>    \>  \>$\arbno{\epsilon},$\\
  189.       \>  \>    \>\go{1}$\wrong{wrong number of arguments}\rangle$\\
  190.       \>  \>$\hbox{ \rm in }\EXP)$\\
  191.       \>$\kappa$\\
  192.       \>$(\fun{update}\:(\fun{new}\:\sigma\,\vert\,\LOC)
  193.                        \:\fun{unspecified}
  194.                \:\sigma),$\\
  195.   \go{3}$\wrong{out of memory}\:\sigma
  196. \end{semfun}
  197. \begin{semfun}
  198. \Esem\sembrack{\hbox{\tt(lambda (\arbno{\I} {\bf.}\ \I) \arbno{\C} $\E_0$)}} =$\\
  199.  \go{1}$\lambda\rho\kappa\:.\:\lambda\sigma\:.\:$\\
  200.   \go{2}$\fun{new}\:\sigma\:\elem\:\LOC\rightarrow$\\
  201.    \go{3}$\fun{send}\:
  202.      $\=$(\langle
  203.          $\=$\fun{new}\:\sigma\,\vert\,\LOC,$\\
  204.       \>  \>$\lambda\arbno{\epsilon}\kappa^\prime\:.\:
  205.            $\=$\#\arbno{\epsilon} \geq \#\arbno{\I}\rightarrow$\\
  206.       \>  \>    \>\go{1}$\fun{tievalsrest}$\\
  207.       \>  \>    \>\go{2}\=$(\lambda\arbno{\alpha}\:.\:
  208.                $\=$(\lambda\rho^\prime\:.\:\Csem\sembrack{\arbno{\C}}\rho^\prime
  209.                    (\Esem\sembrack{\E_0}\rho^\prime\kappa^\prime))$\\
  210.       \>  \>    \>       \> \>$(\fun{extends}\:\rho
  211.                    \:(\arbno{\I}\:\S\:\langle\I\rangle)
  212.                    \:\arbno{\alpha}))$\\
  213.       \>  \>    \>       \>$\arbno{\epsilon}$\\
  214.       \>  \>    \>       \>$(\#\arbno{\I}),$\\
  215.       \>  \>    \>\go{1}$\wrong{too few arguments}\rangle\hbox{ \rm in }\EXP)$\\
  216.       \>$\kappa$\\
  217.       \>$(\fun{update}\:(\fun{new}\:\sigma\,\vert\,\LOC)
  218.                        \:\fun{unspecified}
  219.                \:\sigma),$\\
  220.   \go{3}$\wrong{out of memory}\:\sigma
  221. \end{semfun}
  222. \begin{semfun}
  223. \Esem\sembrack{\hbox{\tt(lambda \I{} \arbno{\C} $\E_0$)}} =
  224.  \Esem\sembrack{\hbox{\tt(lambda ({\bf.}\ \I) \arbno{\C} $\E_0$)}}
  225. \end{semfun}
  226. \begin{semfun}
  227. \Esem\sembrack{\hbox{\tt(\ide{if} $\E_0$ $\E_1$ $\E_2$)}} =$\\
  228.  \go{1}$\lambda\rho\kappa\:.\:
  229.    \Esem\sembrack{\E_0}\:\rho\:(\fun{single}\:(\lambda\epsilon\:.\:
  230.     $\=$\fun{truish}\:\epsilon\rightarrow\Esem\sembrack{\E_1}\rho\kappa,$\\
  231.      \>\go{1}$\Esem\sembrack{\E_2}\rho\kappa))
  232. \end{semfun}
  233. \begin{semfun}
  234. \Esem\sembrack{\hbox{\tt(if $\E_0$ $\E_1$)}} =$\\
  235.  \go{1}$\lambda\rho\kappa\:.\:
  236.    \Esem\sembrack{\E_0}\:\rho\:(\fun{single}\:(\lambda\epsilon\:.\:
  237.     $\=$\fun{truish}\:\epsilon\rightarrow\Esem\sembrack{\E_1}\rho\kappa,$\\
  238.      \>\go{1}$\fun{send}\:\fun{unspecified}\:\kappa))
  239. \end{semfun}
  240. Here and elsewhere, any expressed value other than {\it undefined} may
  241. be used in place of {\it unspecified}.
  242. \begin{semfun}
  243. \Esem\sembrack{\hbox{\tt(\ide{set!} \I{} \E)}} =$\\
  244.  \go{1}$\lambda\rho\kappa\:.\:\Esem\sembrack{\E}\:\rho\:
  245.      (\fun{single}(\lambda\epsilon\:.\:\fun{assign}\:
  246.        $\=$(\fun{lookup}\:\rho\:\I)$\\
  247.     \>$\epsilon$\\
  248.     \>$(\fun{send}\:\fun{unspecified}\:\kappa)))
  249. \end{semfun}
  250. \begin{semfun}
  251. \arbno{\Esem}\sembrack{\:} =
  252.   \lambda\rho\kappa\:.\:\kappa\langle\:\rangle
  253. \end{semfun}
  254. \begin{semfun}
  255. \arbno{\Esem}\sembrack{\E_0\:\arbno{\E}} =$\\
  256.  \go{1}$\lambda\rho\kappa\:.\:
  257.       \Esem\sembrack{\E_0}\:\rho\:
  258.          (\fun{single}
  259.         (\lambda\epsilon_0\:.\:\arbno{\Esem}\sembrack{\arbno{\E}}
  260.         \:\rho\:(\lambda\arbno{\epsilon}\:.\:
  261.                    \kappa\:(\langle\epsilon_0\rangle\:\S\:\arbno{\epsilon}))))
  262. \end{semfun}
  263. \begin{semfun}
  264. \Csem\sembrack{\:} = \lambda\rho\theta\,.\:\theta
  265. \end{semfun}
  266. \begin{semfun}
  267. \Csem\sembrack{\C_0\:\arbno{\C}} =
  268.   \lambda\rho\theta\:.\:\Esem\sembrack{\C_0}\:\rho\:(\lambda\arbno{\epsilon}\:.\:
  269.    \Csem\sembrack{\arbno{\C}}\rho\theta)
  270. \end{semfun}
  271. \egroup  % end smallish
  272. \subsection{Auxiliary functions}
  273. \bgroup\small
  274. \begin{semfun}
  275. \fun{lookup}        :  \ENV \to \Ide \to \LOC$\\$
  276. \fun{lookup} =
  277.  \lambda\rho\I\:.\:\rho\I
  278. \end{semfun}
  279. \begin{semfun}
  280. \fun{extends}       :  \ENV \to \arbno{\Ide} \to \arbno{\LOC} \to \ENV$\\$
  281. \fun{extends} =$\\
  282.  \go{1}$\lambda\rho\arbno{\I}\arbno{\alpha}\:.\:
  283.    $\=$\#\arbno{\I}=0\rightarrow\rho,$\\
  284.     \>$\go{1}\fun{extends}\:(\rho[(\arbno{\alpha}\elt 1)/(\arbno{\I}\elt 1)])
  285.                    \:(\arbno{\I}\drop 1)
  286.                    \:(\arbno{\alpha}\drop 1)
  287. \end{semfun}
  288. \begin{semfun}
  289. \fun{wrong}  :  \ERR \to \CC    \hbox{\qquad [implementation-dependent]}
  290. \end{semfun}
  291. \begin{semfun}
  292. \fun{send}          :  \EXP \to \EC \to \CC$\\$
  293. \fun{send} =
  294.  \lambda\epsilon\kappa\:.\:\kappa\langle\epsilon\rangle
  295. \end{semfun}
  296. \begin{semfun}
  297. \fun{single}        :  (\EXP \to \CC) \to \EC$\\$
  298. \fun{single} =$\\
  299.  \go{1}$\lambda\psi\arbno{\epsilon}\:.\:
  300.    $\=$\#\arbno{\epsilon}=1\rightarrow\psi(\arbno{\epsilon}\elt 1),$\\
  301.     \>$\go{1}\wrong{wrong number of return values}
  302. \end{semfun}
  303. \begin{semfun}
  304. \fun{new}           :  \STO \to (\LOC + \{ \fun{error} \})
  305.     \hbox{\qquad [implementation-dependent]}
  306. \end{semfun}
  307. \begin{semfun}
  308. \fun{hold}          :  \LOC \to \EC \to \CC$\\$
  309. \fun{hold} =
  310.  \lambda\alpha\kappa\sigma\:.\:\fun{send}\,(\sigma\alpha\elt 1)\kappa\sigma
  311. \end{semfun}
  312. \begin{semfun}
  313. \fun{assign}        :  \LOC \to \EXP \to \CC \to \CC$\\$
  314. \fun{assign} =
  315.  \lambda\alpha\epsilon\theta\sigma\:.\:\theta(\fun{update}\:\alpha\epsilon\sigma)
  316. \end{semfun}
  317. \begin{semfun}
  318. \fun{update}        :  \LOC \to \EXP \to \STO \to \STO$\\$
  319. \fun{update} =
  320.  \lambda\alpha\epsilon\sigma\:.\:\sigma[\langle\epsilon,\fun{true}\rangle/\alpha]
  321. \end{semfun}
  322. \begin{semfun}
  323. \fun{tievals}       :  (\arbno{\LOC} \to \CC) \to \arbno{\EXP} \to \CC$\\$
  324. \fun{tievals} =$\\
  325.  \go{1}$\lambda\psi\arbno{\epsilon}\sigma\:.\:
  326.    $\=$\#\arbno{\epsilon}=0\rightarrow\psi\langle\:\rangle\sigma,$\\
  327.     \>$\fun{new}\:\sigma\:\elem\:\LOC\rightarrow\fun{tievals}\,
  328.        $\=$(\lambda\arbno{\alpha}\:.\:\psi(\langle\fun{new}\:\sigma\:\vert\:\LOC\rangle
  329.                      \:\S\:\arbno{\alpha}))$\\
  330.     \>  \>$(\arbno{\epsilon}\drop 1)$\\
  331.     \>  \>$(\fun{update}(\fun{new}\:\sigma\:\vert\:\LOC)
  332.                      (\arbno{\epsilon}\elt 1)
  333.                  \sigma),$\\
  334.     \>$\go{1}\wrong{out of memory}\sigma
  335. \end{semfun}
  336. \begin{semfun}
  337. \fun{tievalsrest}   :  (\arbno{\LOC} \to \CC) \to \arbno{\EXP} \to \NAT \to \CC$\\$
  338. \fun{tievalsrest} =$\\
  339.  \go{1}$\lambda\psi\arbno{\epsilon}\nu\:.\:\fun{list}\:
  340.    $\=$(\fun{dropfirst}\:\arbno{\epsilon}\nu)$\\
  341.     \>$(\fun{single}(\lambda\epsilon\:.\:\fun{tievals}\:\psi\:
  342.            ((\fun{takefirst}\:\arbno{\epsilon}\nu)\:\S\:\langle\epsilon\rangle)))
  343. \end{semfun}
  344. \begin{semfun}
  345. \fun{dropfirst} =
  346.  \lambda l n \:.\:  n=0 \rightarrow l, \fun{dropfirst}\,(l \drop 1)(n - 1)
  347. \end{semfun}
  348. \begin{semfun}
  349. \fun{takefirst} =
  350.  \lambda l n \:.\: n=0 \rightarrow \langle\:\rangle,
  351.      \langle l \elt 1\rangle\:\S\:(\fun{takefirst}\,(l \drop 1)(n - 1))
  352. \end{semfun}
  353. \begin{semfun}
  354. \fun{truish}        :  \EXP \to \TRU$\\$
  355. \fun{truish} =
  356.   \lambda\epsilon\:.\:
  357. %    (\epsilon = \fun{false}\vee\epsilon = \fun{null})\rightarrow
  358.      \epsilon = \fun{false}\rightarrow
  359.           \fun{false},
  360.           \fun{true}
  361. \end{semfun}
  362. \begin{semfun}
  363. \fun{permute}       :  \arbno{\Exp} \to \arbno{\Exp}
  364.     \hbox{\qquad [implementation-dependent]}
  365. \end{semfun}
  366. \begin{semfun}
  367. \fun{unpermute}     :  \arbno{\EXP} \to \arbno{\EXP}
  368.     \hbox{\qquad [inverse of \fun{permute}]}
  369. \end{semfun}
  370. \begin{semfun}
  371. \fun{applicate}     :  \EXP \to \arbno{\EXP} \to \EC \to \CC$\\$
  372. \fun{applicate} =$\\
  373.  \go{1}$\lambda\epsilon\arbno{\epsilon}\kappa\:.\:
  374.    $\=$\epsilon\:\elem\:\FUN\rightarrow(\epsilon\:\vert\:\FUN\elt 2)\arbno{\epsilon}\kappa,
  375.           \wrong{bad procedure}
  376. \end{semfun}
  377. \begin{semfun}
  378. \fun{onearg}      :  (\EXP \to \EC \to \CC) \to (\arbno{\EXP} \to \EC \to \CC)$\\$
  379. \fun{onearg} =$\\
  380.  \go{1}$\lambda\zeta\arbno{\epsilon}\kappa\:.\:
  381.    $\=$\#\arbno{\epsilon}=1\rightarrow\zeta(\arbno{\epsilon}\elt 1)\kappa,$\\
  382.     \>$\go{1}\wrong{wrong number of arguments}
  383. \end{semfun}
  384. \begin{semfun}
  385. \fun{twoarg}      :  (\EXP \to \EXP \to \EC \to \CC) \to (\arbno{\EXP} \to \EC \to \CC)$\\$
  386. \fun{twoarg} =$\\
  387.  \go{1}$\lambda\zeta\arbno{\epsilon}\kappa\:.\:
  388.    $\=$\#\arbno{\epsilon}=2\rightarrow\zeta(\arbno{\epsilon}\elt 1)(\arbno{\epsilon}\elt 2)\kappa,$\\
  389.     \>$\go{1}\wrong{wrong number of arguments}
  390. \end{semfun}
  391. \begin{semfun}
  392. \fun{list}          :  \arbno{\EXP} \to \EC \to \CC$\\$
  393. \fun{list} =$\\
  394.  \go{1}$\lambda\arbno{\epsilon}\kappa\:.\:
  395.    $\=$\#\arbno{\epsilon}=0\rightarrow\fun{send}\:\fun{null}\:\kappa,$\\
  396.     \>$\go{1}\fun{list}\,(\arbno{\epsilon}\drop 1)
  397.              (\fun{single}(\lambda\epsilon\:.\:
  398.                    \fun{cons}\langle\arbno{\epsilon}\elt 1,\epsilon\rangle\kappa))
  399. \end{semfun}
  400. \begin{semfun}
  401. \fun{cons}          :  \arbno{\EXP} \to \EC \to \CC$\\$
  402. \fun{cons} =$\\
  403.  \go{1}$\fun{twoarg}\,(\lambda\epsilon_1\epsilon_2\kappa\sigma\:.\:
  404.    $\=$\fun{new}\:\sigma\:\elem\:\LOC\rightarrow$\\
  405.     \> \go{1}
  406.         \=$(\lambda\sigma^\prime\:.\:
  407.            $\=$\fun{new}\:\sigma^\prime\:\elem\:\LOC\rightarrow$\\
  408.     \>  \>  \>$\go{1}\fun{send}\,
  409.            $\=$($\=$\langle\fun{new}\:\sigma\:\vert\:\LOC,
  410.                         \fun{new}\:\sigma^\prime\:\vert\:\LOC,
  411.          \fun{true}\rangle$\\
  412.                 \>  \>  \>  \>  \>$\hbox{ \rm in }\EXP)$\\
  413.     \>  \>  \>  \>$\kappa$\\
  414.     \>  \>  \>  \>$(\fun{update}(\fun{new}\:\sigma^\prime\:\vert\:\LOC)
  415.                          \epsilon_2
  416.                      \sigma^\prime),$\\
  417.     \>  \>  \>$\go{1}\wrong{out of memory}\sigma^\prime)$\\
  418.     \>  \>$(\fun{update}(\fun{new}\:\sigma\:\vert\:\LOC)\epsilon_1\sigma),$\\
  419.     \>$\go{1}\wrong{out of memory}\sigma)
  420. \end{semfun}
  421. \begin{semfun}
  422. \fun{less}          :  \arbno{\EXP} \to \EC \to \CC$\\$
  423. \fun{less} =$\\
  424.  \go{1}$\fun{twoarg}\,(\lambda\epsilon_1\epsilon_2\kappa\:.\:
  425.    $\=$(\epsilon_1\:\elem\:\NUM\wedge\epsilon_2\:\elem\:\NUM)\rightarrow$\\
  426.     \>$\go{1}\fun{send}\,
  427.            (\epsilon_1\:\vert\:\NUM<\epsilon_2\:\vert\:\NUM\rightarrow
  428.                \fun{true},
  429.            \fun{false})
  430.            \kappa,$\\
  431.     \>$\go{1}\wrong{non-numeric argument to \ide{<}})
  432. \end{semfun}
  433. \begin{semfun}
  434. \fun{add}          :  \arbno{\EXP} \to \EC \to \CC$\\$
  435. \fun{add} =$\\
  436.  \go{1}$\fun{twoarg}\,(\lambda\epsilon_1\epsilon_2\kappa\:.\:
  437.    $\=$(\epsilon_1\:\elem\:\NUM\wedge\epsilon_2\:\elem\:\NUM)\rightarrow$\\
  438.     \>$\go{1}\fun{send}\,
  439.        $\=$((\epsilon_1\:\vert\:\NUM+\epsilon_2\:\vert\:\NUM)\hbox{ \rm in }\EXP)
  440.            \kappa,$\\
  441.     \>$\go{1}\wrong{non-numeric argument to \ide{+}})
  442. \end{semfun}
  443. \begin{semfun}
  444. \fun{car}          :  \arbno{\EXP} \to \EC \to \CC$\\$
  445. \fun{car} =$\\
  446.  \go{1}$\fun{onearg}\,(\lambda\epsilon\kappa\:.\:
  447.    $\=$\epsilon\:\elem\:\PAI\rightarrow
  448.           \fun{hold}\, (\epsilon\:\vert\:\PAI\elt 1) \kappa,$\\
  449.     \>$\go{1}\wrong{non-pair argument to \ide{car}})
  450. \end{semfun}
  451. \begin{semfun}
  452. \fun{cdr}          :  \arbno{\EXP} \to \EC \to \CC %$\\$
  453. \hbox{\qquad [similar to \fun{car}]}
  454. \end{semfun}
  455. \begin{semfun}
  456. \fun{setcar}          :  \arbno{\EXP} \to \EC \to \CC$\\$
  457. \fun{setcar} =$\\
  458.  \go{1}$\fun{twoarg}\,(\lambda\epsilon_1\epsilon_2\kappa\:.\:
  459.    $\=$\epsilon_1\:\elem\:\PAI\rightarrow$\\
  460.     \>$(\epsilon_1\:\vert\:\PAI\elt 3)\rightarrow
  461.           \fun{assign}\,$\=$(\epsilon_1\:\vert\:\PAI\elt 1)$\\
  462.     \>                         \>$\epsilon_2$\\
  463.     \>                            \>$(\fun{send}\:\fun{unspecified}\:\kappa),$\\
  464.     \>$\wrong{immutable argument to \ide{set-car!}},$\\
  465.     \>$\wrong{non-pair argument to \ide{set-car!}})
  466. \end{semfun}
  467. \begin{semfun}
  468. \fun{eqv}          :  \arbno{\EXP} \to \EC \to \CC$\\$
  469. \fun{eqv} =$\\
  470.  \go{1}$\fun{twoarg}\,(\lambda\epsilon_1\epsilon_2\kappa\:.\:
  471.    $\=$(\epsilon_1\:\elem\:\MSC\wedge\epsilon_2\:\elem\:\MSC)\rightarrow$\\
  472.     \>$\go{1}\fun{send}\,
  473.        $\=$(\epsilon_1\:\vert\:\MSC = \epsilon_2\:\vert\:\MSC\rightarrow\fun{true},
  474.             \fun{false})\kappa,$\\
  475.     \>$(\epsilon_1\:\elem\:\SYM\wedge\epsilon_2\:\elem\:\SYM)\rightarrow$\\
  476.     \>$\go{1}\fun{send}\,
  477.        $\=$(\epsilon_1\:\vert\:\SYM = \epsilon_2\:\vert\:\SYM\rightarrow\fun{true},
  478.             \fun{false})\kappa,$\\
  479.     \>$(\epsilon_1\:\elem\:\CHR\wedge\epsilon_2\:\elem\:\CHR)\rightarrow$\\
  480.     \>$\go{1}\fun{send}\,
  481.        $\=$(\epsilon_1\:\vert\:\CHR = \epsilon_2\:\vert\:\CHR \rightarrow\fun{true},
  482.             \fun{false})\kappa,$\\
  483.     \>$(\epsilon_1\:\elem\:\NUM\wedge\epsilon_2\:\elem\:\NUM)\rightarrow$\\
  484.     \>$\go{1}\fun{send}\,
  485.        $\=$(\epsilon_1\:\vert\:\NUM=\epsilon_2\:\vert\:\NUM\rightarrow\fun{true},
  486.             \fun{false})\kappa,$\\
  487.     \>$(\epsilon_1\:\elem\:\PAI\wedge\epsilon_2\:\elem\:\PAI)\rightarrow$\\
  488.     \>$\go{1}\fun{send}\,
  489.        $\=$($\=$(\lambda{p_1}{p_2}\:.\:
  490.                 ($\=$({p_1}\elt 1) = ({p_2}\elt 1)\wedge$\\
  491.     \>  \>   \>   \>$({p_1}\elt 2) = ({p_2}\elt 2))
  492.                      \rightarrow\fun{true},$\\
  493.     \>  \>   \>   \>$\go{1}\fun{false})$\\
  494.     \>  \>   \>$(\epsilon_1\:\vert\:\PAI)$\\
  495.     \>  \>   \>$(\epsilon_2\:\vert\:\PAI))$\\
  496.     \>  \>$\kappa,$\\
  497.     \>$(\epsilon_1\:\elem\:\VEC\wedge\epsilon_2\:\elem\:\VEC)\rightarrow
  498. %\fun{send}\,
  499. %       $\=$((\#(\epsilon_1\:\vert\:\VEC)=\#(\epsilon_2\:\vert\:\VEC)
  500. %         \wedge\hbox{\rm Y}(\lambda\fun{loop}\:.\:\lambda\fun{v1}\fun{v2}\:.\:
  501. %       $\=$\#\fun{v1}=0\rightarrow\fun{true},$\\
  502. %    \>  \>  \>$(\fun{v1}\elt 1) = (\fun{v2}\elt 1)\rightarrow
  503. %       \fun{loop}(\fun{v1}\drop 1)(\fun{v2}\drop 1),$\\
  504. %    \>  \>  \>$\go{1}\fun{false})(\epsilon_1\:\vert\:\VEC)(\epsilon_2\:\vert\:\VEC))
  505. %          \rightarrow\fun{true},$\\
  506. %    \>  \>$\go{1}\fun{false})\kappa
  507. \ldots,$\\
  508.     \>$(\epsilon_1\:\elem\:\STR\wedge\epsilon_2\:\elem\:\STR)\rightarrow
  509. %\fun{send}\,
  510. %       $\=$((\#(\epsilon_1\:\vert\:\STR)=\#(\epsilon_2\:\vert\:\STR)\wedge
  511. %    \hbox{\rm Y}(\lambda\fun{loop}\:.\:\lambda\fun{v1}\fun{v2}\:.\:
  512. %       $\=$\#\fun{v1}=0\rightarrow\fun{true},$\\
  513. %    \>  \>  \>$(\fun{v1}\elt 1) = (\fun{v2}\elt 1)\rightarrow
  514. %     \fun{loop}(\fun{v1}\drop 1)(\fun{v2}\drop 1),$\\
  515. %    \>  \>  \>$\go{1}\fun{false})(\epsilon_1\:\vert\:\STR)(\epsilon_2\:\vert\:\STR))
  516. %      \rightarrow\fun{true},$\\
  517. %    \>  \>$\go{1}\fun{false})\kappa
  518. \ldots,$\\
  519.     \>$(\epsilon_1\:\elem\:\FUN\wedge\epsilon_2\:\elem\:\FUN)\rightarrow$\\
  520.     \>$\go{1}\fun{send}\,
  521.        $\=$((\epsilon_1\:\vert\:\FUN\elt 1) = (\epsilon_2\:\vert\:\FUN\elt 1)
  522.                \rightarrow\fun{true},
  523.                       \fun{false})$\\
  524.     \>  \>$\kappa,$\\
  525.     \>$\go{1}\fun{send}\,\:\fun{false}\:\kappa)
  526. \end{semfun}
  527. \begin{semfun}
  528. \fun{apply}          :  \arbno{\EXP} \to \EC \to \CC$\\$
  529. \fun{apply} =$\\
  530.  \go{1}$\fun{twoarg}\,(\lambda\epsilon_1\epsilon_2\kappa\:.\:
  531.    $\=$\epsilon_1\:\elem\:\FUN\rightarrow
  532.          \fun{valueslist}\,\langle\epsilon_2\rangle
  533.             (\lambda\arbno{\epsilon}\:.\:\fun{applicate}\:\epsilon_1\arbno{\epsilon}\kappa),$\\
  534.     \>$\go{1}\wrong{bad procedure argument to \ide{apply}})
  535. \end{semfun}
  536. \begin{semfun}
  537. \fun{valueslist}          :  \arbno{\EXP} \to \EC \to \CC$\\$
  538. \fun{valueslist} =$\\
  539.  \go{1}$\fun{onearg}\,(\lambda\epsilon\kappa\:.\:
  540.    $\=$\epsilon\:\elem\:\PAI\rightarrow$\\
  541.     \>$\go{1}\fun{cdr}
  542.          $\=$\langle\epsilon\rangle$\\
  543.     \>    \>$(\lambda\arbno{\epsilon}\:.\:
  544.               $\=$\fun{valueslist}\:$\\
  545.     \>    \>       \>$\arbno{\epsilon}$\\
  546.     \>    \>       \>$(\lambda\arbno{\epsilon}\:.\:\fun{car}\langle\epsilon\rangle
  547.         (\fun{single}(\lambda\epsilon\:.\:
  548.           \kappa(\langle\epsilon\rangle\:\S\:\arbno{\epsilon}))))),$\\
  549.     \>$\epsilon = \fun{null}\rightarrow\kappa\langle\:\rangle,$\\
  550.     \>$\go{1}\wrong{non-list argument to \ide{values-list}})
  551. \end{semfun}
  552. \begin{semfun}
  553. \fun{cwcc}          :  \arbno{\EXP} \to \EC \to \CC
  554.     \hbox{\qquad [\ide{call-with-current-continuation}]}$\\$
  555. \fun{cwcc} =$\\
  556.  \go{1}$\fun{onearg}\,(\lambda\epsilon\kappa\:.\:
  557.    $\=$\epsilon\:\elem\:\FUN\rightarrow$\\
  558.     \>$\go{1}(\lambda\sigma\:.\:
  559.        $\=$\fun{new}\:\sigma\:\elem\:\LOC\rightarrow$\\
  560.     \>  \>$\go{1}\fun{applicate}\:
  561.        $\=$\epsilon$\\
  562.     \>  \>  \>$\langle\langle\fun{new}\:\sigma\:\vert\:\LOC,
  563.                  \lambda\arbno{\epsilon}\kappa^\prime\:.\:
  564.                  \kappa\arbno{\epsilon}\rangle
  565.               \hbox{ \rm in }\EXP\rangle$\\
  566.     \>  \>  \>$\kappa$\\
  567.     \>  \>  \>$(\fun{update}\,
  568.             $\=$(\fun{new}\:\sigma\:\vert\:\LOC)$\\
  569.     \>    \>  \>     \>$\fun{unspecified}$\\
  570.     \>    \>  \>     \>$\sigma),$\\
  571.     \>  \>$\go{1}\wrong{out of memory}\,\sigma),$\\
  572.     \>$\go{1}\wrong{bad procedure argument})
  573. \end{semfun}
  574. \egroup  % end smallish
  575. \egroup
  576.